FOO.LSP[W82,JMC] - www.SailDart.org

perm filename FOO.LSP[W82,JMC] blob sn#632549 filedate 1982-01-11 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	proof? 
C00015 00003	(∀e phi |λu.(u*v)*w = u*(v*w)| listinduction nil sortinfo)
C00023 ENDMK
C⊗;
proof? 
* LISPX started.
* 
* 
* 
* 
* 
* 
* 
* 
* 
* 
* 
* 12. ∀U.SEXP U
    ctxt: (1 11)   deps: NIL

* 
;Loading LET 90
* 13. ∀X U.LISTP X~U
    ctxt: (1 2 7 10)   deps: NIL

* 
* 
* 14. ∀U.NULL U≡U=NNIL
    ctxt: (1 5 9)   deps: NIL

* 15. NULL NNIL
    ctxt: (5 9)   deps: NIL

* 
* 16. ∀X Y.SEXP X~Y
    ctxt: (2 7 11)   deps: NIL

* 
* 17. ∀X Y.¬ATOM X~Y
    ctxt: (2 7 9)   deps: NIL

* 
* 
* 18. ∀X U.¬NULL X~U
    ctxt: (1 2 7 9)   deps: NIL

* 
* 
* 19. ∀X U.CAR (X~U)=X
    ctxt: (1 2 7 8)   deps: NIL

* 
* 20. ∀X U.CDR (X~U)=U
    ctxt: (1 2 7 8)   deps: NIL

* 
* 21. ∀X Y.CAR (X~Y)=X
    ctxt: (2 7 8)   deps: NIL

* 
* 
* 22. ∀X Y.CDR (X~Y)=Y
    ctxt: (2 7 8)   deps: NIL

* 
* 
* 23. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))
    ctxt: (1 2 4 5 7)   deps: NIL

* 
* 24. ∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))
    ctxt: (2 4 7 9)   deps: NIL

* 
* 
* 26. ∀U V.LISTP U*V
    ctxt: (1 10 25)   deps: NIL

* 
* 27. ∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)
    ctxt: (1 7 8 9 25)   deps: NIL

* 
* 
* 
* 30. ∀X.LISTP LIST(X)
    ctxt: (2 10 29)   deps: NIL

* 
* 31. ∀X.LIST(X)=X~NNIL
    ctxt: (2 5 7 29)   deps: NIL

* 
* 32. ∀X Y.LISTP LIST(X,Y)
    ctxt: (2 10 29)   deps: NIL

* 
* 33. ∀X Y.LIST(X,Y)=X~LIST(Y)
    ctxt: (2 7 29)   deps: NIL

* 
* 34. ∀X Y Z.LISTP LIST(X,Y,Z)
    ctxt: (2 10 29)   deps: NIL

* 
* 35. ∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)
    ctxt: (2 7 29)   deps: NIL

* 
* 36. ∀U.LISTP REVERSE U
    ctxt: (1 10 28)   deps: NIL

* 
* 37. ∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)
    ctxt: (1 5 8 9 25 28 29)   deps: NIL

* 
* 38. ∀U.NNIL*U=U
    ctxt: (1 5 25)   deps: NIL

* 
* 
* 39. ∀X U V.X~U*V=X~(U*V)
    ctxt: (1 2 7 25)   deps: NIL

* 
* 
* 40. ∀U V W.(U*V)*W=U*(V*W)
    ctxt: (1 25)   deps: NIL

* 41. ∀U V.REVERSE (U*V)=REVERSE V*REVERSE U
    ctxt: (1 25 28)   deps: NIL

* 
* 43. ∀X U.FLAT(X,U)=IF ATOM X THEN X~U ELSE FLAT(CAR X,FLAT(CDR X,U))
    ctxt: (1 2 7 8 9 42)   deps: NIL

* 
* 
* 45. ∀X.FLATTEN(X)=IF ATOM X THEN LIST(X) ELSE FLATTEN(CAR X)*FLATTEN(CDR X)
    ctxt: (2 8 9 25 29 44)   deps: NIL

* 
* 46. ∀X U.LISTP FLAT(X,U)
    ctxt: (1 2 10 42)   deps: NIL

* 
;;; lispx.lsp[f81,jmc] ekl axioms for lisp with infixes

(proof lispx)

(DECL (U u0 u1 u2 u3 v v0 v1 v2 v3 W w0 w1 w2 w3) |ground| variable listp)

(DECL (X Y Z) |GROUND| VARIABLE sEXP)

(DECL (A B C) |GROUND| VARIABLE)

(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)

(DECL (NNIL) |GROUND| CONsTANT LIsTp)

(DECL (CONs) |GROUND⊗GROUND→GROUND| CONsTANT)

(DECL (~) |GROUND⊗GROUND→GROUND| CONsTANT NIL INFIX 850)

(DECL (CAR CDR) |GROUND→GROUND| CONsTANT nil unary 950)

(DECL (ATOM NULL) |GROUND→TRUTHVAL| CONsTANT nil unary 750)

(DECL (LIsTp) |GROUND→TRUTHVAL| CONsTANT nil unary 750)

(DECL (sEXP) |GROUND→TRUTHVAL| CONsTANT nil unary 750)

(AXIOM |∀U.sEXP U |)
(lname sortinfo *)

(AXIOM |∀X U.LISTP X~U |)
(lname sortinfo (sortinfo *))
(lname simpinfo (*))

(AXIOM |∀U.NULL U ≡ U=NNIL|)

(axiom |null nnil|)
(lname simpinfo (* simpinfo))

(AXIOM |∀X Y.SEXP X~Y|)
(lname sortinfo (sortinfo *))

(AXIOM |∀X Y.¬ATOM X~Y|)
(lname consfacts *)
(lname simpinfo (* simpinfo))

(AXIOM |∀X U.¬NULL X~U|)
(lname consfacts (* consfacts))
(lname simpinfo (* simpinfo))

(AXIOM |∀X U.CAR (X ~ U) = X|)
(lname simpinfo (* simpinfo))

(AXIOM |∀X U.CDR (X~U) = U|)
(lname simpinfo (* simpinfo))

(AXIOM |∀X Y.CAR (X ~ Y) = X|)
(lname consfacts (* consfacts))
(lname simpinfo (* simpinfo))

(AXIOM |∀X Y.CDR (X~Y) = Y|)
(lname consfacts (* consfacts))
(lname simpinfo (* simpinfo))

(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))|)
(lname listinduction (*))

(AXIOM |∀PHI.(∀X.ATOM X ⊃ PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))|)
(lname sexpinduction (*))

;;; Common defined functions

(DECL (*) |GROUND⊗GROUND→GROUND| CONsTANT NIL INFIX 840)

(axiom |∀u v.listp(u*v)|)
(lname sortinfo (sortinfo *))

(AXIOM |∀U V.(U*V)=IF NULL(U) THEN V ELsE CAR U ~ (CDR U *V)|)
(lname definfo (*))

(decl (reverse) |ground→ground| constant nil unary 950)

(decl list |ground* → ground| functional)

(axiom |∀x.listp(list(x))|)
(lname sortinfo (sortinfo *))

(axiom |∀x.list(x) = x~nnil|)
(lname simpinfo (* simpinfo))

(axiom |∀x y.listp(list(x,y))|)
(lname sortinfo (sortinfo *))

(axiom |∀x y.list(x,y) = x~list(y)|)
(lname simpinfo (* simpinfo))

(axiom |∀x y z.listp(list(x,y,z))|)
(lname sortinfo (sortinfo *))

(axiom |∀x y z.list(x,y,z) = x~list(y,z)|)
(lname simpinfo (* simpinfo))

(axiom |∀u.listp(reverse(u))|)
(lname sortinfo (sortinfo *))

(axiom |∀u.reverse(u) = if null(u) then nnil
else reverse(cdr u) * list(car u)|)
(lname definfo (* definfo))

;;; theorems taken as axioms for further proofs

(axiom |∀u.nnil*u=u|)
(lname appendfacts (*))
(lname simpinfo (* simpinfo))

(axiom |∀x u v.x~u*v = x~(u*v)|)
(lname appendfacts (appendfacts *))
(lname simpinfo (* simpinfo))

(axiom |∀u v w.(u*v)*w = u*(v*w)|)

(axiom |∀u v.reverse(u*v) = reverse v * reverse u|)

;;; flat(x,u) has an imbedded call
(decl (flat) |ground⊗ground→ground| constant)
(axiom |∀x u.flat(x,u) = if atom x then x~u else flat(car x,flat(cdr x, u))|)
(lname definfo (* definfo))
(decl (flatten) |ground → ground| constant)
(axiom |∀x.flatten(x) = if atom x then list(x)
				else flatten(car x)*flatten(cdr x)|)
(lname definfo (* definfo))

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))*nil*([1#2#1#2]($definfo**sortinfo))
**simpinfo*nil*([1](der))*nil|
 sortinfo)
;;;;
47. (∀X.ATOM X⊃(∀U.X~U=LIST(X)*U))∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X~Y,U)=FLATTEN(X~Y)*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    ctxt: (1 2 7 9 25 29 42 44)   deps: NIL

* 48. (∀X.ATOM X⊃(∀U.X~U=LIST(X)*U))∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X~Y,U)=FLATTEN(X~Y)*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    ctxt: (1 2 7 9 25 29 42 44)   deps: NIL

* ;PDL-OVERFLOW
QUIT
* .....done.
* 
proof? 
* .....done.LISPX read in 
proof? 
* switched to LISPX
* 
(proof lispx)
49. (∀X.ATOM X⊃(∀U.X~U=LIST(X)*U))∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X~Y,U)=FLATTEN(X~Y)*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    ctxt: (1 2 7 9 25 29 42 44)   deps: NIL

* 50. (∀X.ATOM X⊃(∀U.X~U=X~NNIL*U))∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X~Y,U)=FLATTEN(X~Y)*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    ctxt: (1 2 5 7 9 25 42 44)   deps: NIL

* 51. (∀X.ATOM X⊃(∀U.X~U=X~LIST(Y1,Z)*U))∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X~Y,U)=FLATTEN(X~Y)*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    ctxt: (1 2 7 9 25 29 42 44 51)   deps: NIL

* 52. (∀X.ATOM X⊃(∀U.X~U=X~LIST(Y1,Z)*U))∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X~Y,U)=FLATTEN(X~Y)*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    ctxt: (1 2 7 9 25 29 42 44 52)   deps: NIL

* 
(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1]($definfo*$definfo*$definfo*$simpinfo**sortinfo))*nil|
 sortinfo)
proof? 
.....done.LISPX read in 
proof? 
* switched to LISPX
* 
(proof lispx)
49. LIST(X)*U=X~NNIL*U
    ctxt: (1 2 5 7 25 29)   deps: NIL

* 50. LIST(X)*U=IF NULL X~NNIL THEN U ELSE CAR (X~NNIL)~(CDR (X~NNIL)*U)
    ctxt: (1 2 5 7 8 9 25 29)   deps: NIL

* 51. LIST(X)*U=X~U
    ctxt: (1 2 7 25 29)   deps: NIL

* 52. LIST(X)*U=X~U
    ctxt: (1 2 7 25 29)   deps: NIL

* 
(∀e phi |λu.(u*v)*w = u*(v*w)| listinduction nil sortinfo)
(rw * |*appendfacts*nil| sortinfo)
(trw |∀x u.(u*v)*w = u*(v*w) ⊃ x~((u*v)*w)=x~(u*(v*w))| |der|)
(rw 37 |*38*nil|)
(∀i (v w) )